nLab analytic LPO

Context

Analysis

Constructivism, Realizability, Computability

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Contents

Idea

In real analysis, there is a principle on the Cauchy real numbers which is equivalent in strength to the limited principle of omniscience for natural numbers, and states that the pseudo-order on the Cauchy real numbers is a decidable relation, or that the Cauchy real numbers have decidable tight apartness. This principle can be generalised from the Cauchy real numbers to all notions of real numbers, such as the Dedekind real numbers, and is hence called the analytic limited principle of omniscience, or the analytic LPO. In classical mathematics, all of these are implied by excluded middle; however, in neutral constructive mathematics, the different analytic LPO are different principles of different strength, because the Cauchy and Dedekind real numbers and any other notion of real numbers between the Cauchy and Dedekind real numbers cannot be proven to coincide.

Definition

There are many different notions of real numbers in constructive mathematics. What all these real numbers have in common are that they are an Archimedean ordered field extension RR of the field of (sequential, modulated) Cauchy real numbers R C\mathrm{R}_C; i.e. there are unique ring homomorphisms of ordered fields

CR D\mathbb{R}_C \hookrightarrow R \hookrightarrow \mathbb{R}_D

where D\mathbb{R}_D is the ordered field of Dedekind real numbers - the homomorphism into D\mathbb{R}_D always exists since D\mathbb{R}_D is the terminal Archimedean ordered field. In general the ring homomorphisms are not provably isomorphisms unless the Dedekind real numbers and Cauchy real numbers coincide. Thus, there are many different notions of the analytic limited principle of omniscience; the analytic limited principles of omniscience are defined for each Archimedean ordered field extension of the Cauchy real numbers.

Definition

Let RR be an Archimedean ordered field extension of the field of (sequential, modulated) Cauchy real numbers R C\mathrm{R}_C. The analytic LPO for RR states that the usual apartness relation on RR decidable (xyx \neq y or x=yx = y), or equivalently trichotomy for RR (x<yx \lt y or x=yx = y or x>yx \gt y), or equivalently, that RR is a discrete field.

Warning. Given an Archimedean ordered field extension RR of the field of (sequential, modulated) Cauchy real numbers, the analytic limited principle of omniscience for RR is not to be confused with the limited principle of omniscience for RR - the latter is the statement that for every function ff from RR to the boolean domain, either there exists an element xx in RR such that f(x)=1f(x) = 1, or for all elements xx in RR, f(x)=0f(x) = 0. For RR the Cauchy real numbers, the analytic LPO for the Cauchy real numbers is equivalent to the LPO for the natural numbers, while the LPO for the Cauchy real numbers is much stronger than the LPO for the natural numbers.

Let RR be any Archimedean ordered field extension of the Cauchy real numbers. The analytic LPO also makes sense for any Archimedean ordered local Artinian R R -algebra AA as well, where the relation <\lt is in general only a strict weak order instead of a pseudo-order, the preorder \geq is not a partial order, and the equivalence relation aba \approx b derived from the preorder holds if and only if aba - b is nilpotent. In this case, the analytic LPO for the Weil RR-algebra AA says that the strict weak order on AA is a decidable relation, or that the apartness relation a#ba \# b is a decidable relation, or invertibility is decidable, and the quotient of AA by its nilradical is the field of real numbers RR satisfying the analytic LPO.

Properties

Theorem

The analytic LPO for the (sequential, modulated) Cauchy real numbers C\mathbb{R}_C implies the LPO for natural numbers.

Proof

Let ff be a function from the natural numbers to the boolean domain. Define the sequence uu on the rationals as

u(n)= x=0 kf(n)2 xu(n) = \sum_{x = 0}^k \frac{f(n)}{2^x}

This sequence is a Cauchy sequence with a modulus of continuity, so taking the limit of this Cauchy sequence yields a Cauchy real number [u][u]. The analytic LPO on the Cauchy reals states that either [u]#0[u] \# 0 or [u]=0[u] = 0. In the former case, [u]>12 k[u] \gt \frac{1}{2^k} for some natural number kk so there exists an nn such that f(n)=1f(n) = 1, and in the latter case, f(n)=0f(n) = 0 for all nn. Thus, the LPO for natural numbers hold.

Theorem

Suppose that there is an Archimedean ordered field RR which is a field extension of the Cauchy real numbers C\mathbb{R}_C. Then the analytic LPO for RR implies that RR is isomorphic to C\mathbb{R}_C

Proof

Every Archimedean ordered field is a subfield of the Dedekind real numbers, which means that by coercion one can consider the elements of any Archimedean ordered field to be Dedekind real numbers, which are Dedekind cuts. Theorem 10.6.3 of Booij 2020 says that any Dedekind real number (i.e. Dedekind cut) for which there exists a locator is a Cauchy real number. This implies that given an Archimedean ordered field RR, if for every element in RR there exists a locator, then every element in RR is a Cauchy real number, and RR is a subfield of the Cauchy real numbers. If RR is also a field extension of the Cauchy real numbers, then RR is isomorphic to the Cauchy real numbers, since the Cantor-Schroeder-Bernstein theorem holds for Archimedean ordered fields and ring homomorphisms in the category of Archimedean ordered fields.

The analytic LPO implies that corollary 11.4.3 of UFP 2013 can be proven: If analytic LPO holds then “(x<y)(x<z)+(z<y)(x \lt y) \to (x \lt z) + (z \lt y) can be proved: either x<zx \lt z or ¬(x<z)\neg(x \lt z). In the former case we are done, while in the latter we get z<yz \lt y because zx<yz \leq x \lt y.” Therefore, we get a locator for every element of RR, which then implies that RR is isomorphic to the Cauchy real numbers.

Theorem

Suppose that there are two Archimedean ordered fields RR and RR' such that both are field extensions of the Cauchy real numbers C\mathbb{R}_C and RR' is a field extension of RR. Then, the analytic LPO for RR' implies the analytic LPO for RR.

Proof

Analytic LPO for RR' implies that RR' is isomorphic to the Cauchy real numbers, which implies that any subfield of RR' which is a field extension of the Cauchy real numbers is isomorphic to RR', since the Cantor-Schroeder-Bernstein theorem holds for Archimedean ordered fields and ring homomorphisms in the category of Archimedean ordered fields. Since this is true of RR, this implies that the analytic LPO for RR also holds, since RR' and RR are isomorphic fields.

Lemma

Suppose that there is an Archimedean ordered field RR which is a field extension of the Cauchy real numbers C\mathbb{R}_C. Then, the analytic LPO for RR implies the LPO for natural numbers.

Proof

Since the field of Cauchy real numbers is a (trivial) field extension of itself, the analytic LPO for RR implies the analytic LPO for the Cauchy real numbers, which implies the LPO for the natural numbers.

Let Σ\Sigma be the initial σ \sigma -frame. It is a sub-σ\sigma-frame of the frame of truth values. One can construct a set of Dedekind real numbers R Σ\mathrm{R}_\Sigma out of Dedekind cuts in valued in the initial σ\sigma-frame ΣΩ\Sigma \subseteq \Omega (see section 11.2 of UFP 2013), where then one has ring homomorphisms

R CR ΣR D\mathrm{R}_C \hookrightarrow \mathrm{R}_\Sigma \hookrightarrow \mathrm{R}_D

Theorem

The LPO for natural numbers is equivalent to the boolean domain 𝟚\mathbb{2} being the initial σ\sigma-frame Σ𝟚\Sigma \coloneqq \mathbb{2}.

Proof

Thus, one can use the decidable Dedekind cuts 𝟚× 𝟚\mathbb{Q}^\mathbb{2} \times \mathbb{Q}^\mathbb{2} to construct the Dedekind real numbers, since Σ𝟚\Sigma \cong \mathbb{2} is the initial σ\sigma-frame.

Theorem

The LPO for natural numbers implies the analytic LPO for subset of Dedekind real numbers R Σ D\mathrm{R}_\Sigma \subseteq \mathbb{R}_D constructed out of Dedekind cuts in valued in the initial σ\sigma-frame ΣΩ\Sigma \subseteq \Omega.

Proof

LPO for the natural numbers implies that for each rational number qq, the left and right Dedekind cuts for an element xx of R Σ\mathrm{R}_\Sigma, evaluated at qq, L x(q)L_x(q) and R x(q)R_x(q), are both decidable propositions. In addition, LPO for the natural numbers implies that any existential quantification of a decidable predicate over the rational numbers is itself a decidable proposition. The pseudo-order relation <\lt on Σ\mathbb{R}_\Sigma is defined as

x<yq.L x(q)R y(q)x \lt y \coloneqq \exists q \in \mathbb{Q}.L_x(q) \wedge R_y(q)

Since L x(q)L_x(q) and R y(q)R_y(q) are both decidable, the conjunction is also decidable, and so is the existential quantifier by LPO for the natural numbers, and by definition the strict order on R Σ\mathrm{R}_\Sigma, which is the analytic LPO for R Σ\mathrm{R}_\Sigma.

Theorem

The LPO for natural numbers, the C\mathbb{R}_C-analytic LPO, and the Σ\mathbb{R}_\Sigma-analytic LPO are equivalent to each other.

Proof

We showed that the the C\mathbb{R}_C-analytic LPO implies the LPO for natural numbers, that the Σ\mathbb{R}_\Sigma-analytic LPO implies the C\mathbb{R}_C-analytic LPO, and the LPO for natural numbers implies the Σ\mathbb{R}_\Sigma-analytic LPO. By transitivity of implication, the converses also hold, so all three statements are equivalent to each other.

Theorem

Suppose that there is an Archimedean ordered field RR which is a field extension of the Cauchy real numbers C\mathbb{R}_C. Then the analytic LPO for RR implies that RR is equivalent to C\mathbb{R}_C and Σ\mathbb{R}_\Sigma.

Proof

Analytic LPO for RR implies the LPO for natural numbers, which implies that C\mathbb{R}_C is equivalent to Σ\mathbb{R}_\Sigma. Theorem 11.2.14 in UFP 2013 states that given the initial σ\sigma-frame Σ\Sigma, every Archimedean ordered field which is admissible for Σ\Sigma is a subfield of Σ\mathbb{R}_\Sigma. The LPO for natural numbers implies the initial σ\sigma-frame is the boolean domain, which means that analytic LPO for RR implies that RR is admissible for the boolean domain, and hence a subfield of Σ\mathbb{R}_\Sigma. This means that RR coincides with both C\mathbb{R}_C and Σ\mathbb{R}_\Sigma, since the Cantor-Schroeder-Bernstein theorem holds for Archimedean ordered fields and ring homomorphisms.

Lemma

Suppose that there is an Archimedean ordered field RR which is a field extension of the Cauchy real numbers C\mathbb{R}_C. Then the analytic LPO for RR implies that RR is sequentially Cauchy complete.

Proof

Analytic LPO for RR implies that RR is equivalent to Σ\mathbb{R}_\Sigma. Since Σ\mathbb{R}_\Sigma is constructed out of Dedekind cuts (valued in the initial σ\sigma-frame Σ\Sigma), theorem 11.2.12 and corollary 11.2.13 of UFP 2013 states that Σ\mathbb{R}_\Sigma is sequentially Cauchy complete, which then implies that RR is sequentially Cauchy complete.

Finally, let H\mathbb{R}_H be the HoTT book real numbers, which are the initial sequentially Cauchy complete Archimedean ordered field. Then,

Theorem

The LPO for natural numbers and the analytic LPO for H\mathbb{R}_H are equivalent to each other.

Proof

There is a ring homomorphism H Σ\mathbb{R}_H \hookrightarrow \mathbb{R}_\Sigma because Σ\mathbb{R}_\Sigma is Cauchy complete and H\mathbb{R}_H is initial in the category of Cauchy complete Archimedean ordered fields, and there is a ring homomorphism C H\mathbb{R}_C \hookrightarrow \mathbb{R}_H because the rational numbers are a subset of H\mathbb{R}_H, and C\mathbb{R}_C is the limit of Cauchy sequences of rational numbers (with modulus), while H\mathbb{R}_H is the limit of Cauchy sequences of elements of H\mathbb{R}_H, implying that C\mathbb{R}_C embeds in H\mathbb{R}_H.

Since the LPO for natural numbers is equivalent to the analytic LPO for R Σ\mathrm{R}_\Sigma, this in turn implies that R C\mathrm{R}_C and R Σ\mathrm{R}_\Sigma are isomorphic fields, which implies that H\mathbb{R}_H is isomorphic to R Σ\mathrm{R}_\Sigma, since the Cantor-Schroeder-Bernstein theorem holds for Archimedean ordered fields and ring homomorphisms in the category of Archimedean ordered fields. Thus, the analytic LPO for R Σ\mathrm{R}_\Sigma is equivalent to the analytic LPO for R H\mathrm{R}_H and equivalent to the LPO for natural numbers.

Thus, one has a hierarchy of analytic limited principles of omniscience, where

  • The analytic LPO for the (sequential, modulated) Cauchy real numbers, for the Escardo-Simpson real numbers/HoTT book real numbers, and for the subset of the Dedekind real numbers whose Dedekind cuts are valued in the initial σ\sigma-frame, are all the weakest and equivalent to the LPO for the natural numbers;

  • The analytic LPO for the Dedekind real numbers is the strongest.

  • For any other Archimedean ordered field extension of the Cauchy real numbers RR which is neither equivalent to the Cauchy real numbers or the Dedekind real numbers, the analytic LPO for RR are intermediate in strength between the Cauchy-analytic LPO and the Dedekind-analytic LPO.

Given an Archimedean ordered field extension RR of the Cauchy real numbers, there are other statements related to the analytic LPO for RR:

((x.¬(x#x))(x,y.(x#y)(y#x))(x,y,z.(x#y)(y#z)(x#z)))(x,y.(x#y)¬(x#y))((\forall x.\neg (x \# x)) \wedge (\forall x, y.(x \# y) \Rightarrow (y \# x)) \wedge (\forall x, y, z.(x \# y) \wedge (y \# z) \Rightarrow (x \# z))) \Rightarrow (\forall x, y.(x \# y) \vee \neg (x \# y))

Models

References

The phrase “analytic LPO” is mentioned in the following paper, although in that paper it actually refer to the analytic WLPO (the reals have decidable equality) instead of the actual analytic LPO (the reals have decidable tight apartness). In addition, it makes the wrong statement that LPO is equivalent to Cauchy reals having decidable equality; it is WLPO which is equivalent to Cauchy reals having decidable equality (i.e. analytic WLPO for Cauchy reals), while LPO is equivalent to Cauchy reals having decidable tight apartness.

Last revised on August 20, 2024 at 22:47:36. See the history of this page for a list of all contributions to it.